Date: Wed, 20 Nov 1996 19:15:08 GMT
Server: Apache/1.0.3
Content-type: text/html
Content-length: 2064
Last-modified: Thu, 25 Apr 1996 15:00:00 GMT

<html>
<HEAD><TITLE> Structurally Free Logic </TITLE></HEAD>
<BODY background = "pentag8.gif">
<H2> Structurally Free Logic </H2>



<Strong>Description: </Strong> <Blockquote> In the last few years
there has been great interest in so-called "substructural logics,"
whereby various well-known logics are distinguished by the structural
rules that are postulated in the Gentzen systems for the logics. Most
notorious have been thinning (relevance logic), contraction (BCK
logic), and linear logic (linear logic). But there is no reason to
stop there, as people have considered non-commutative linear logic
(better, the associative Lambek calculus), and people have even looked
at non-associative logice. The point of view taken in this project is
that structural rules should be done away with altogether, and their
place taken by explicit introduction rules for
combinators. Combinators are take as "first-class' objects, and still
a cut-elimination theorem can be proven.

Further the ternary relational semantics (Routley-Meyer semantics)
for the Lambek calculus can be extended so as to provide a semantics
for combinatory logic. The key idea is that a ternary relation on
states can be interpreted as an indexed action on states. So a set of
states (a proposition) can be simultaneously be viewed as a set of
actions, and so it makes sense to talk of applying one proposition to
another (even itself).

There are still a number of open problems, mostly centering about the
addition of conjunction and disjunction. These include proving the cut-
theorem with respect to the distributive combination of the two, and 
providing a completeness theorem for their non-distributive combination.
</Blockquote>
<P>

<Strong>Associated Faculty:</Strong>
Michael Dunn
<P>

<Strong> Affiliated Projects: </Strong> Robert K. Meyer
(Automated Reasoning Project, Australian National University)
<P>

<Strong> Support: </Strong> 
College of Arts and Sciences
<p> 

<!WA0><A HREF = "http://www.cs.indiana.edu/l/www/research/index.html"><!WA1><IMG SRC="http://www.cs.indiana.edu/research/back.gif">Return to Computer Science Research Page  </A>


